To reduce clock power consumption many designers use clock enable signals to clock gate flip flops. To implement clock gating it is necessary to identify enable signals in the design. Typically, designers include some explicit enable signals in a circuit design which can be identified by looking at the combinational logic of a particular flip-flop (FF). Such explicit enable signals that are identifiable by looking at the combinational logic of an FF are referred to as combinational enable signals. These combinational enable signals are usually identified during the synthesis phase of the design process. The second class of enable signals is sequential enable signals. These enable signals can be identified by looking at the sequential behavior of the design. As soon as an enable signal, combinational or sequential, has been identified it can be used to clock gate the FF.
Power reduction tools typically identify potential clock gating and provide the user of the power reduction tools with the enable signal equations needed to clock-gate the FF. The user can perform the clock gating by implementing it manually or by instructing the power reduction tool to change the design automatically.
To verify the insertion of clock gating resulting from the identification of enable signals, equivalence checking is needed in order to verify that the design without clock gating, i.e., the golden design, is equivalent to the design with clock gating, i.e., the implementation design. As combinational clock gating does not change the state function, combinational equivalence checking (CEC) is sufficient to perform equivalence checking of the golden design versus the implementation design. Sequential clock gating changes the state function and hence, sequential equivalence checking (SEC) is needed to verify such kind of transformation. Applying full SEC may be runtime consuming and not scalable for large design.
It would therefore be advantageous to provide a solution for SEC which is runtime efficient. It would be further beneficial if such a solution is scalable to large circuit designs.